/****************************************************************************
 * Elisa 1.0                                                                *
 *--------------------------------------------------------------------------*
 * Author: Laurent Granvilliers, Vincent Sorin                              *
 * Copyright (c) 2004 Laboratoire d'Informatique de Nantes Atlantique       *
 *--------------------------------------------------------------------------*
 * Elisa is distributed WITHOUT ANY WARRANTY. Read the associated           *
 * COPYRIGHT file for more details.                                         *
 *--------------------------------------------------------------------------*
 * elisa_solver.cpp                                                         *
 ****************************************************************************/

#include "elisa_solver.h"
#include "elisa_time.h"

#include <fstream>
#include "elisa_variable.h"

USING_ELISA

//--------------------------------------------------------------------------
// class Solver
//--------------------------------------------------------------------------

bool Solver::reduce()
{
	if (m_reduction) {

		m_searchTree.prepareReduce();
		m_reduction->initActive();
		bool res = m_reduction->apply();

		m_model->updateSymbolicDomain();

		//reduce_count++;
		
#ifdef ELISA_PROFILE_REDUCE
		VarImplSet vars;
		m_model->toVariables(vars);
		VarImplSet::iterator vit = vars.begin();
		while (vit != vars.end())
		{
			VarImplPtr vip = *vit;
			m_reduceOut << vip->getSymbolicRep()->getName() << "::" << std::endl;
			m_reduceOut << *(vip->getSearchTree()->domain<Interval>(vip->getIndexDomain())) << std::endl;
			++vit;
		}
		m_reduceOut << std::endl;
#endif

		return res;

	} else {
#ifdef ELISA_PROFILE_REDUCE
		m_reduceOut << "reduce failed!" << std::endl;
#endif

		return false;
	}
}

bool Solver::solve()
{
	reset();
	while (next()) {}
	return (m_numSol > 0);
}

bool Solver::next()
{
	// no domain already processed?
	if (m_numDom == 0) {

		if (m_searchTree.isEmpty())
			reset();
	}

	if (m_numSol > 0) {
		// discard the last solution
		(*m_backTrack)();
		(*m_move)();
	}

	// Loop until a solution box is computed
	while (!m_searchTree.isEmpty()) {
		++m_numDom;

		// Reduction
		if (reduce()) {

			// Reduction ok, is the box a solution?
			if (this->isSolution()) {
				m_searchOutput->handle(++m_numSol);
				m_model->updateSymbolicDomain();

				return true;

			} else {
				// Reduction ok, but the box is not a solution => splitting

#ifdef ELISA_PROFILE
				++m_numSplit;
#endif

				// Compute the next variable to split
				(*m_makeNeighborhood)();
				(*m_move)();
			}
		} else {
			// Reduction => inconsistency
			(*m_backTrack)();
			(*m_move)();
		}
	}

	return false; // no more solution
}
